YES 19.696 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,r)→r

is transformed to
r0 (_,r) = r

The following Lambda expression
\(n,_)→n

is transformed to
n0 (n,_) = n

The following Lambda expression
\(_,r)→r

is transformed to
r1 (_,r) = r

The following Lambda expression
\(q,_)→q

is transformed to
q1 (q,_) = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if r > 0 then n + 1 else n

is transformed to
ceiling0 True = n + 1
ceiling0 False = n

The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
frac@(Double wy wz)

is replaced by the following term
Double wy wz

The bind variable of the following binding Pattern
frac@(Float xu xv)

is replaced by the following term
Float xu xv



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare0 x y True = GT

compare3 x y = compare2 x y (x == y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw

gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vvz vwu = gcd3 vvz vwu
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw
gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

gcd1 True vvz vwu = error []
gcd1 vwv vww vwx = gcd0 vww vwx

gcd2 True vvz vwu = gcd1 (vwu == 0) vvz vwu
gcd2 vwy vwz vxu = gcd0 vwz vxu

gcd3 vvz vwu = gcd2 (vvz == 0) vvz vwu
gcd3 vxv vxw = gcd0 vxv vxw

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal0 x True = `negate` x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ LetRed

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
ceiling0 (r > 0)
where 
ceiling0 True = n + 1
ceiling0 False = n
n  = n0 vu8
n0 (n,vw) = n
r  = r0 vu8
r0 (vv,r) = r
vu8  = properFraction x

are unpacked to the following functions on top level
ceilingR0 vxx (vv,r) = r

ceilingN vxx = ceilingN0 vxx (ceilingVu8 vxx)

ceilingCeiling0 vxx True = ceilingN vxx + 1
ceilingCeiling0 vxx False = ceilingN vxx

ceilingN0 vxx (n,vw) = n

ceilingVu8 vxx = properFraction vxx

ceilingR vxx = ceilingR0 vxx (ceilingVu8 vxx)

The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2Reduce0 vxy vxz x y True = x `quot` reduce2D vxy vxz :% (y `quot` reduce2D vxy vxz)

reduce2Reduce1 vxy vxz x y True = error []
reduce2Reduce1 vxy vxz x y False = reduce2Reduce0 vxy vxz x y otherwise

reduce2D vxy vxz = gcd vxy vxz

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw
gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

are unpacked to the following functions on top level
gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd' x vuz = gcd0Gcd'2 x vuz
gcd0Gcd' x y = gcd0Gcd'0 x y

gcd0Gcd'2 x vuz = gcd0Gcd'1 (vuz == 0) x vuz
gcd0Gcd'2 vvx vvy = gcd0Gcd'0 vvx vvy

gcd0Gcd'1 True x vuz = x
gcd0Gcd'1 vvu vvv vvw = gcd0Gcd'0 vvv vvw

The bindings of the following Let/Where expression
(fromIntegral q,r :% y)
where 
q  = q1 vu30
q1 (q,zu) = q
r  = r1 vu30
r1 (zv,r) = r
vu30  = quotRem x y

are unpacked to the following functions on top level
properFractionR1 vyu vyv (zv,r) = r

properFractionQ vyu vyv = properFractionQ1 vyu vyv (properFractionVu30 vyu vyv)

properFractionVu30 vyu vyv = quotRem vyu vyv

properFractionR vyu vyv = properFractionR1 vyu vyv (properFractionVu30 vyu vyv)

properFractionQ1 vyu vyv (q,zu) = q



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
HASKELL
                          ↳ NumRed

mainModule Main
  ((ceiling :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
HASKELL
                              ↳ Narrow

mainModule Main
  (ceiling :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vyw30000), Succ(vyw18000)) → new_primPlusNat(vyw30000, vyw18000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(Succ(vyw42300), Succ(vyw44000)) → new_esEs(vyw42300, vyw44000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vyw31100)) → new_primMulNat(vyw31100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS(vyw5620, vyw5630)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ DependencyGraphProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Zero) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS(Succ(Zero), Zero) → new_primModNatS(new_primMinusNatS1, Zero)
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)
new_primModNatS0(vyw562, vyw563, Zero, Zero) → new_primModNatS00(vyw562, vyw563)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
QDP
                                          ↳ UsableRulesProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ RuleRemovalProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + 2·x1   
POL(Zero) = 0   
POL(new_primMinusNatS0(x1)) = 2 + 2·x1   
POL(new_primModNatS(x1, x2)) = x1 + x2   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ RuleRemovalProof
QDP
                                                      ↳ PisEmptyProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
QDP
                                          ↳ UsableRulesProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Zero) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)
new_primModNatS0(vyw562, vyw563, Zero, Zero) → new_primModNatS00(vyw562, vyw563)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Zero) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)
new_primModNatS0(vyw562, vyw563, Zero, Zero) → new_primModNatS00(vyw562, vyw563)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ QDPOrderProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Zero) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw562, vyw563, Zero, Zero) → new_primModNatS00(vyw562, vyw563)
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Zero) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw562, vyw563, Zero, Zero) → new_primModNatS00(vyw562, vyw563)
The remaining pairs can at least be oriented weakly.

new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primMinusNatS2(x1, x2)) = x1   
POL(new_primModNatS(x1, x2)) = x1   
POL(new_primModNatS0(x1, x2, x3, x4)) = 1 + x1   
POL(new_primModNatS00(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ QDPOrderProof
QDP
                                                      ↳ DependencyGraphProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(vyw562, vyw563) → new_primModNatS(new_primMinusNatS2(vyw562, vyw563), Succ(vyw563))
new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ QDPOrderProof
                                                    ↳ QDP
                                                      ↳ DependencyGraphProof
QDP
                                                          ↳ UsableRulesProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ QDPOrderProof
                                                    ↳ QDP
                                                      ↳ DependencyGraphProof
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
QDP
                                                              ↳ QReductionProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ QDPOrderProof
                                                    ↳ QDP
                                                      ↳ DependencyGraphProof
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
QDP
                                                                  ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw562, vyw563, Succ(vyw5640), Succ(vyw5650)) → new_primModNatS0(vyw562, vyw563, vyw5640, vyw5650)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ DependencyGraphProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))
new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS1, Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
QDP
                                          ↳ UsableRulesProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ RuleRemovalProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + 2·x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1 + x2   
POL(new_primMinusNatS0(x1)) = 2 + 2·x1   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ RuleRemovalProof
QDP
                                                      ↳ PisEmptyProof
                                        ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
QDP
                                          ↳ UsableRulesProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS1Zero
new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS0(x0)
new_primMinusNatS1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ Rewriting
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578)) at position [0] we obtained the following new rules:

new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
QDP
                                                      ↳ Rewriting
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(Succ(vyw577), Succ(vyw578)), Succ(vyw578)) at position [0] we obtained the following new rules:

new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
QDP
                                                          ↳ QDPOrderProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Zero) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw577, vyw578) → new_primDivNatS(new_primMinusNatS2(vyw577, vyw578), Succ(vyw578))
The remaining pairs can at least be oriented weakly.

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1   
POL(new_primDivNatS0(x1, x2, x3, x4)) = 1 + x1   
POL(new_primDivNatS00(x1, x2)) = 1 + x1   
POL(new_primMinusNatS2(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)
new_primMinusNatS2(Zero, Zero) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ QDPOrderProof
QDP
                                                              ↳ DependencyGraphProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Zero, Zero) → new_primDivNatS00(vyw577, vyw578)
new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ QDPOrderProof
                                                            ↳ QDP
                                                              ↳ DependencyGraphProof
QDP
                                                                  ↳ UsableRulesProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)

The TRS R consists of the following rules:

new_primMinusNatS2(Succ(vyw5620), Succ(vyw5630)) → new_primMinusNatS2(vyw5620, vyw5630)
new_primMinusNatS2(Zero, Succ(vyw5630)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vyw5620), Zero) → Succ(vyw5620)

The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ QDPOrderProof
                                                            ↳ QDP
                                                              ↳ DependencyGraphProof
                                                                ↳ QDP
                                                                  ↳ UsableRulesProof
QDP
                                                                      ↳ QReductionProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ QDPOrderProof
                                                            ↳ QDP
                                                              ↳ DependencyGraphProof
                                                                ↳ QDP
                                                                  ↳ UsableRulesProof
                                                                    ↳ QDP
                                                                      ↳ QReductionProof
QDP
                                                                          ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw577, vyw578, Succ(vyw5790), Succ(vyw5800)) → new_primDivNatS0(vyw577, vyw578, vyw5790, vyw5800)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling0(vyw587, vyw588, Succ(vyw5890), Succ(vyw5900), ba) → new_ceilingCeiling0(vyw587, vyw588, vyw5890, vyw5900, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling00(vyw572, vyw573, Succ(vyw5740), Succ(vyw5750), ba) → new_ceilingCeiling00(vyw572, vyw573, vyw5740, vyw5750, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling01(vyw582, vyw583, Succ(vyw5840), Succ(vyw5850), ba) → new_ceilingCeiling01(vyw582, vyw583, vyw5840, vyw5850, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling02(vyw567, vyw568, Succ(vyw5690), Succ(vyw5700), ba) → new_ceilingCeiling02(vyw567, vyw568, vyw5690, vyw5700, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: